<!DOCTYPE html>





<html lang="zh-CN">
<head>
  <meta charset="UTF-8">
<meta name="viewport" content="width=device-width, initial-scale=1, maximum-scale=2">
<meta name="theme-color" content="#222">
<meta name="generator" content="Hexo 3.9.0">
  <link rel="apple-touch-icon" sizes="180x180" href="/images/apple-touch-icon-next.png?v=7.4.0">
  <link rel="icon" type="image/png" sizes="32x32" href="/images/favicon-32x32.png?v=7.4.0">
  <link rel="icon" type="image/png" sizes="16x16" href="/images/favicon-16x16.png?v=7.4.0">
  <link rel="mask-icon" href="/images/avatar.svg?v=7.4.0" color="#222">
  <link rel="alternate" href="/atom.xml" title="Anemone's Blog" type="application/atom+xml">
  <meta name="google-site-verification" content="Re5JdegRYzNFco-rC9lYIsvSWIgh5JvyfhuEaZCeFCk">
  <meta name="baidu-site-verification" content="opTC8YN3Pn">

<link rel="stylesheet" href="/css/main.css?v=7.4.0">


<link rel="stylesheet" href="https://cdn.bootcss.com/font-awesome/4.7.0/css/font-awesome.min.css">


<script id="hexo-configurations">
  var NexT = window.NexT || {};
  var CONFIG = {
    root: '/',
    scheme: 'Pisces',
    version: '7.4.0',
    exturl: false,
    sidebar: {"position":"left","display":"post","offset":12,"onmobile":false},
    copycode: {"enable":false,"show_result":false,"style":null},
    back2top: {"enable":true,"sidebar":false,"scrollpercent":false},
    bookmark: {"enable":false,"color":"#222","save":"auto"},
    fancybox: false,
    mediumzoom: false,
    lazyload: false,
    pangu: false,
    algolia: {
      appID: 'GB90MXPJ1C',
      apiKey: '05d808da3baf50ac2f2fad2dc3a3cd8f',
      indexName: 'dev_blog',
      hits: {"per_page":20},
      labels: {"input_placeholder":"Search for Posts","hits_empty":"We didn't find any results for the search: ${query}","hits_stats":"${hits} results found in ${time} ms"}
    },
    localsearch: {"enable":false,"trigger":"auto","top_n_per_article":1,"unescape":true,"preload":false},
    path: 'search.xml',
    motion: {"enable":true,"async":false,"transition":{"post_block":"fadeIn","post_header":"slideDownIn","post_body":"slideDownIn","coll_header":"slideLeftIn","sidebar":"slideUpIn"}},
    translation: {
      copy_button: '复制',
      copy_success: '复制成功',
      copy_failure: '复制失败'
    },
    sidebarPadding: 40
  };
</script>

  <meta name="description" content="Iterative Algorithm 对于一个含 $k$ 个节点的CFG，每个迭代算法对于每个node $n$ 更新$\mathrm{OUT}[n]$。  假设迭代算法的研究对象（domain）是$V$，定义一个k元组  V^k=\left(\mathrm{OUT}\left[\mathrm{n}_{1}\right], \mathrm{OUT}\left[\mathrm{n}_{2}\righ">
<meta name="keywords" content="白盒扫描,静态程序分析,数据流分析,PL">
<meta property="og:type" content="article">
<meta property="og:title" content="静态程序分析课程笔记（数据流分析-理论基础）">
<meta property="og:url" content="http://anemone.top/pl-静态程序分析课程笔记（数据流分析-理论基础）/index.html">
<meta property="og:site_name" content="Anemone&#39;s Blog">
<meta property="og:description" content="Iterative Algorithm 对于一个含 $k$ 个节点的CFG，每个迭代算法对于每个node $n$ 更新$\mathrm{OUT}[n]$。  假设迭代算法的研究对象（domain）是$V$，定义一个k元组  V^k=\left(\mathrm{OUT}\left[\mathrm{n}_{1}\right], \mathrm{OUT}\left[\mathrm{n}_{2}\righ">
<meta property="og:locale" content="zh-CN">
<meta property="og:image" content="http://anemone.top/pl-静态程序分析课程笔记（数据流分析-理论基础）/image-20200804204606009.png">
<meta property="og:image" content="http://anemone.top/pl-静态程序分析课程笔记（数据流分析-理论基础）/image-20200812205336289.png">
<meta property="og:image" content="http://anemone.top/pl-静态程序分析课程笔记（数据流分析-理论基础）/image-20200812214731510.png">
<meta property="og:image" content="http://anemone.top/pl-静态程序分析课程笔记（数据流分析-理论基础）/image-20200814215920162.png">
<meta property="og:image" content="http://anemone.top/pl-静态程序分析课程笔记（数据流分析-理论基础）/image-20200814220329588.png">
<meta property="og:image" content="http://anemone.top/pl-静态程序分析课程笔记（数据流分析-理论基础）/image-20200815173321586.png">
<meta property="og:updated_time" content="2020-10-18T04:04:24.629Z">
<meta name="twitter:card" content="summary">
<meta name="twitter:title" content="静态程序分析课程笔记（数据流分析-理论基础）">
<meta name="twitter:description" content="Iterative Algorithm 对于一个含 $k$ 个节点的CFG，每个迭代算法对于每个node $n$ 更新$\mathrm{OUT}[n]$。  假设迭代算法的研究对象（domain）是$V$，定义一个k元组  V^k=\left(\mathrm{OUT}\left[\mathrm{n}_{1}\right], \mathrm{OUT}\left[\mathrm{n}_{2}\righ">
<meta name="twitter:image" content="http://anemone.top/pl-静态程序分析课程笔记（数据流分析-理论基础）/image-20200804204606009.png">
  <link rel="canonical" href="http://anemone.top/pl-静态程序分析课程笔记（数据流分析-理论基础）/">


<script id="page-configurations">
  // https://hexo.io/docs/variables.html
  CONFIG.page = {
    sidebar: "",
    isHome: false,
    isPost: true,
    isPage: false,
    isArchive: false
  };
</script>

  <title>静态程序分析课程笔记（数据流分析-理论基础） | Anemone's Blog</title>
  








  <noscript>
  <style>
  .use-motion .brand,
  .use-motion .menu-item,
  .sidebar-inner,
  .use-motion .post-block,
  .use-motion .pagination,
  .use-motion .comments,
  .use-motion .post-header,
  .use-motion .post-body,
  .use-motion .collection-header { opacity: initial; }

  .use-motion .logo,
  .use-motion .site-title,
  .use-motion .site-subtitle {
    opacity: initial;
    top: initial;
  }

  .use-motion .logo-line-before i { left: initial; }
  .use-motion .logo-line-after i { right: initial; }
  </style>
</noscript>

</head>

<body itemscope itemtype="http://schema.org/WebPage" lang="zh-CN">
  <div class="container use-motion">
    <div class="headband"></div>

    <header id="header" class="header" itemscope itemtype="http://schema.org/WPHeader">
      <div class="header-inner"><div class="site-brand-container">
  <div class="site-meta">

    <div>
      <a href="/" class="brand" rel="start">
        <span class="logo-line-before"><i></i></span>
        <span class="site-title">Anemone's Blog</span>
        <span class="logo-line-after"><i></i></span>
      </a>
    </div>
  </div>

  <div class="site-nav-toggle">
    <button aria-label="切换导航栏">
      <span class="btn-bar"></span>
      <span class="btn-bar"></span>
      <span class="btn-bar"></span>
    </button>
  </div>
</div>


<nav class="site-nav">
  
  <ul id="menu" class="menu">
      
      
      
        
        <li class="menu-item menu-item-home">
      
    

    <a href="/" rel="section"><i class="fa fa-fw fa-home"></i>首页</a>

  </li>
      
      
      
        
        <li class="menu-item menu-item-about">
      
    

    <a href="/about/" rel="section"><i class="fa fa-fw fa-user"></i>关于</a>

  </li>
      
      
      
        
        <li class="menu-item menu-item-tags">
      
    

    <a href="/tags/" rel="section"><i class="fa fa-fw fa-tags"></i>标签</a>

  </li>
      
      
      
        
        <li class="menu-item menu-item-categories">
      
    

    <a href="/categories/" rel="section"><i class="fa fa-fw fa-th"></i>分类</a>

  </li>
      
      
      
        
        <li class="menu-item menu-item-archives">
      
    

    <a href="/archives/" rel="section"><i class="fa fa-fw fa-archive"></i>归档</a>

  </li>
      <li class="menu-item menu-item-search">
        <a href="javascript:;" class="popup-trigger">
        
          <i class="fa fa-search fa-fw"></i>搜索</a>
      </li>
    
  </ul>

</nav>
  <div class="site-search">
    <div class="popup search-popup">
    <div class="search-header">
  <span class="search-icon">
    <i class="fa fa-search"></i>
  </span>
  <div class="search-input" id="search-input"></div>
  <span class="popup-btn-close">
    <i class="fa fa-times-circle"></i>
  </span>
</div>
<div class="algolia-results">
  <div id="algolia-stats"></div>
  <div id="algolia-hits"></div>
  <div id="algolia-pagination" class="algolia-pagination"></div>
</div>

  
</div>
<div class="search-pop-overlay"></div>

  </div>
</div>
    </header>

    
  <div class="back-to-top">
    <i class="fa fa-arrow-up"></i>
    <span>0%</span>
  </div>
  <div class="reading-progress-bar"></div>


    <main id="main" class="main">
      <div class="main-inner">
        <div class="content-wrap">
            

          <div id="content" class="content">
            

  <div id="posts" class="posts-expand">
      <article itemscope itemtype="http://schema.org/Article">
  
  
  
  <div class="post-block post">
    <link itemprop="mainEntityOfPage" href="http://anemone.top/pl-静态程序分析课程笔记（数据流分析-理论基础）/">

    <span hidden itemprop="author" itemscope itemtype="http://schema.org/Person">
      <meta itemprop="name" content="Anemone">
      <meta itemprop="description" content="关注Web安全、移动安全、Fuzz测试和机器学习">
      <meta itemprop="image" content="/images/avatar.jpg">
    </span>

    <span hidden itemprop="publisher" itemscope itemtype="http://schema.org/Organization">
      <meta itemprop="name" content="Anemone's Blog">
    </span>
      <header class="post-header">
        <h2 class="post-title" itemprop="name headline">静态程序分析课程笔记（数据流分析-理论基础）

          
        </h2>

        <div class="post-meta">
            <span class="post-meta-item">
              <span class="post-meta-item-icon">
                <i class="fa fa-calendar-o"></i>
              </span>
              <span class="post-meta-item-text">发表于</span>

              
                
              

              <time title="创建时间：2020-08-02 17:34:13" itemprop="dateCreated datePublished" datetime="2020-08-02T17:34:13+08:00">2020-08-02</time>
            </span>
          
            

            
              <span class="post-meta-item">
                <span class="post-meta-item-icon">
                  <i class="fa fa-calendar-check-o"></i>
                </span>
                <span class="post-meta-item-text">更新于</span>
                <time title="修改时间：2020-10-18 12:04:24" itemprop="dateModified" datetime="2020-10-18T12:04:24+08:00">2020-10-18</time>
              </span>
            
          
            <span class="post-meta-item">
              <span class="post-meta-item-icon">
                <i class="fa fa-folder-o"></i>
              </span>
              <span class="post-meta-item-text">分类于</span>
              
                <span itemprop="about" itemscope itemtype="http://schema.org/Thing"><a href="/categories/Program-Language/" itemprop="url" rel="index"><span itemprop="name">Program Language</span></a></span>

                
                
              
            </span>
          

          
            <span id="/pl-静态程序分析课程笔记（数据流分析-理论基础）/" class="post-meta-item leancloud_visitors" data-flag-title="静态程序分析课程笔记（数据流分析-理论基础）" title="阅读次数">
              <span class="post-meta-item-icon">
                <i class="fa fa-eye"></i>
              </span>
              <span class="post-meta-item-text">阅读次数：</span>
              <span class="leancloud-visitors-count"></span>
            </span>
          

        </div>
      </header>

    
    
    
    <div class="post-body" itemprop="articleBody">

      
        <h1 id="Iterative-Algorithm"><a href="#Iterative-Algorithm" class="headerlink" title="Iterative Algorithm"></a>Iterative Algorithm</h1><ul>
<li><p>对于一个含 $k$ 个节点的CFG，每个迭代算法对于每个node $n$ 更新$\mathrm{OUT}[n]$。</p>
</li>
<li><p>假设迭代算法的研究对象（domain）是$V$，定义一个k元组<br>  <script type="math/tex">V^k=\left(\mathrm{OUT}\left[\mathrm{n}_{1}\right], \mathrm{OUT}\left[\mathrm{n}_{2}\right], \ldots, \mathrm{OUT}\left[\mathrm{n}_{\mathrm{k}}\right]\right)$，$V^k\in(V_1 \times V_2 \times \dots \times V_k)</script>，<br>  $ V^k $ 即一次迭代产生的输出，每次迭代会更新$V^k$，可以将每次迭代经过transfer functions和control-flow handing的过程抽象为$F: V^k\rightarrow {V^{k}}’$</p>
</li>
<li><p>当$V^k\rightarrow {V^{k}}’$时，即$X=F(X)$ ，称$F(x)$在$X$处到达了<strong>不动点</strong>，$X$为$F(x)$的不动点，</p>
</li>
</ul><a id="more"></a>
<h1 id="Poset-amp-partial-order（偏序集和偏序）"><a href="#Poset-amp-partial-order（偏序集和偏序）" class="headerlink" title="Poset &amp; partial order（偏序集和偏序）"></a>Poset &amp; partial order（偏序集和偏序）</h1><blockquote>
<p>We define <strong>poset</strong> as a pair (P, ⊑) where ⊑ is a binary relation that defines a partial ordering over P, and ⊑ has the following properties: </p>
<p>(1) $\forall x \in P, x \sqsubseteq x$  (Reflexivity, 自反性)<br>(2) $\forall x, y \in P, x \sqsubseteq y \wedge y \sqsubseteq x \Rightarrow x=y \quad$ (Antisymmetry，反对称性)<br>(3) $\forall x,y,z \in P, x \sqsubseteq y \wedge y \sqsubseteq z \Rightarrow x \sqsubseteq z $ (Transitivity，传递性)</p>
</blockquote>
<p><strong>偏序集</strong>为一个二元组$(P, \sqsubseteq)$，$P$为一集合，$\sqsubseteq$为在集合上的一种比较关系，这个二元组为偏序集当且仅当集合元素在关系上满足自反性、反对称性和传递性。</p>
<p><strong>偏序</strong>的含义：一个集合中的任意两个元素不一定存在顺序关系（任意两元素不一定能比较大小）</p>
<h1 id="Uppper-and-Lower-Bounds（上界和下界）"><a href="#Uppper-and-Lower-Bounds（上界和下界）" class="headerlink" title="Uppper and Lower Bounds（上界和下界）"></a>Uppper and Lower Bounds（上界和下界）</h1><blockquote>
<p>Given a poset (P, ⊑) and its subset $S$ that  $S\subseteq P$, we say that $u\in P$ is an <strong>upper bound</strong> of $S$, if $\forall x \in P, x\sqsubseteq u$. Similarly, $l∈P$ is an <strong>lower bound</strong> of $S$, if $\forall x \in P, l\sqsubseteq u$.</p>
</blockquote>
<p>如图，$\{a,b,c\}$是$S$的上界（灰色），$\{\}$是$S$的下界：</p>
<p><img src="/pl-静态程序分析课程笔记（数据流分析-理论基础）/image-20200804204606009.png" alt="image-20200804204606009"></p>
<h2 id="最小上界、最大下界"><a href="#最小上界、最大下界" class="headerlink" title="最小上界、最大下界"></a>最小上界、最大下界</h2><blockquote>
<p>We define the <strong>least upper bound (lub or join)</strong> of $S$, written $⊔S$, if for every upper bound of $S$, say $u, ⊔S⊑u$. Similarly, We define the <strong>greatest lower bound (glb or meet)</strong> of $S$, written $⊓S$, if for every lower bound of $S$, say $l, l⊑⊓S$.</p>
</blockquote>
<p>特别的，对于仅有两个元素的集合$S=\{a,b\}$，$\sqcup S$ 可以写为$a \sqcup b$，同理 $\sqcap S$可以写为 $a\sqcap b$。</p>
<p><strong>注意：</strong>（最小）上界和（最大）下界是针对集合中的特定子集的，而上下界本身不一定在子集中，并且：</p>
<ul>
<li>不是所有偏序集均存在lub或者glb（如先前灰色的集合就不含lub）</li>
<li>如果一个偏序集存在lub和glb，那么它是唯一的<ul>
<li>证明： 设$g_1$ 和$g_2$ 同为 P 的glb，那么根据定义 $g_1\sqsubseteq (g_2 = \sqcap P)$ 并且$g_2\sqsubseteq (g_1 = \sqcap P)$，又因为反对称性，所以$g_1=g_2$</li>
</ul>
</li>
</ul>
<h1 id="Lattice-Semilattice-Complete-and-Product-Lattice"><a href="#Lattice-Semilattice-Complete-and-Product-Lattice" class="headerlink" title="Lattice, Semilattice, Complete and Product Lattice"></a>Lattice, Semilattice, Complete and Product Lattice</h1><h2 id="Lattice（格）"><a href="#Lattice（格）" class="headerlink" title="Lattice（格）"></a>Lattice（格）</h2><blockquote>
<p>Given a poset $(P, ⊑), ∀a,b∈P$, if $a⊔b$ and $a⊓b$ exist, then $(P,⊑)$ is called a lattice. </p>
</blockquote>
<p>如果一个偏序集的任意两个元素都有最小上界和最大下界，那么这一偏序集是一个<strong>格</strong></p>
<h2 id="Semilattice"><a href="#Semilattice" class="headerlink" title="Semilattice"></a>Semilattice</h2><p>最小上界和最大下界只存在一个的偏序集称<strong>半格</strong>，只存在最小上界称为“join semilattice”，只存在最大下界称为“meet semilattice”。</p>
<h2 id="Complete-Lattice，top-amp-bottom（全格，-top-和-perp-）"><a href="#Complete-Lattice，top-amp-bottom（全格，-top-和-perp-）" class="headerlink" title="Complete Lattice，top &amp; bottom（全格，$\top$ 和 $\perp$）*"></a>Complete Lattice，top &amp; bottom（全格，$\top$ 和 $\perp$）*</h2><blockquote>
<p>Given a lattice $(P,⊑)$, for arbitrary subset $S$ of $P$, if $⊔S$ and $⊓S$ exist, then $(P,⊑)$ is called a complete lattice.</p>
</blockquote>
<p>一个偏序集的任意子集均存在最小上界和最大下界，那么这个偏序集成为<strong>全格</strong>。</p>
<p>每个全格都存在一个最大元素 top（$\top=\sqcup P$）和最小元素bottom（$\perp=\sqcap P$）</p>
<p>所有元素有限的格（finite lattice）均是全格。（反之不成立）</p>
<h2 id="Product-Lattice"><a href="#Product-Lattice" class="headerlink" title="Product Lattice"></a>Product Lattice</h2><blockquote>
<p>Given lattices $L_1=(P_1,⊑_1),L_2=(P_2,⊑_2),…,L_n=(P_n,⊑)n)$, if for all $i$, $(P_i,⊑_i)$ has $⊔i$(least upper bound) and $⊓_i$(greatest lower bound), then we can have a product lattice $L^n=(P,⊑)$ that is defined by:</p>
<ul>
<li>$P=P_{1} \times \ldots \times P_{n}$</li>
<li>$\left(x_{1}, \ldots, x_{n}\right) \sqsubseteq\left(y_{1}, \ldots, y_{n}\right) \Leftrightarrow\left(x_{1} \sqsubseteq y_{1}\right) \wedge \ldots \wedge\left(x_{n} \sqsubseteq y_{n}\right)$</li>
<li>$\left(x_{1}, \ldots, x_{n}\right) \sqcup\left(y_{1}, \ldots, y_{n}\right)=\left(x_{1} \sqcup_{1} y_{1}, \ldots, x_{n} \cup_{n} y_{n}\right)$</li>
<li>$\left(x_{1}, \ldots, x_{n}\right) \sqcap\left(y_{1}, \ldots, y_{n}\right)=\left(x_{1} \sqcap_{1} y_{1}, \ldots, x_{n} \sqcap_{n} y_{n}\right)$</li>
</ul>
</blockquote>
<p>Product Lattice仍是Lattice，若每个子格为全格，那么乘积也是全格。</p>
<h1 id="Data-Flow-Analysis-Framework-via-Lattice"><a href="#Data-Flow-Analysis-Framework-via-Lattice" class="headerlink" title="Data Flow Analysis Framework via Lattice"></a>Data Flow Analysis Framework via Lattice</h1><p>一个数据流分析框架可以表示为一个三元组$(D,L,F)$ ，其中：</p>
<ul>
<li>D：指数据流分析的方向，i.e., forward or backward；</li>
<li>L：指lattice，该格表示所有domain值域，以及meet（$\sqcap$）或join（$\sqcup$）操作；</li>
<li>F：一组transfer function。</li>
</ul>
<h1 id="Monotonicity-and-Fixed-Point-Theorem"><a href="#Monotonicity-and-Fixed-Point-Theorem" class="headerlink" title="Monotonicity and Fixed Point Theorem"></a>Monotonicity and Fixed Point Theorem</h1><h2 id="Monotonicity（单调性）"><a href="#Monotonicity（单调性）" class="headerlink" title="Monotonicity（单调性）"></a>Monotonicity（单调性）</h2><blockquote>
<p>A function $f: L→L$ ($L$ is a lattice) is monotonic if $∀x,y∈L$,  $x⊑y⟹f(x)⊑f(y)$</p>
</blockquote>
<p>普通函数的单调性的推广</p>
<h2 id="Fixed-Point-Theorem"><a href="#Fixed-Point-Theorem" class="headerlink" title="Fixed-Point Theorem"></a>Fixed-Point Theorem</h2><blockquote>
<p>Given a complete lattice ($L,⊑$), if (1) $f:L→L$ is monotonic and (2) $L$ is finite, then the <strong>least fixed point</strong> of $f$ can be found by iterating $f(⊥), f(f(⊥)), \dots, f^k(⊥)$ until a fixed point is reached the greatest fixed point of $f$ can be found by iterating $f(\top),f(f(\top)),\dots, f^k(\top)$ until a fixed point is reached.</p>
</blockquote>
<p>如果f单调且L有界，那么f存在不动点，从$⊥$开始迭代执行$f$可得最小不动点，从$\top$开始迭代可得最大不动点。</p>
<p>证明：<br>(1) Existence<br>由$\perp$定义以及$f:L\rightarrow L$可得</p>
<script type="math/tex; mode=display">
\perp \sqsubseteq f(\perp)</script><p>又因$f$是单调的，因此</p>
<script type="math/tex; mode=display">
f(\perp) \sqsubseteq f(f(\perp))=f^2(\perp)</script><p>由于L是有限(finite)的，因此总会存在一个k，有</p>
<script type="math/tex; mode=display">
f^{Fix}=f^k(\perp)=f^{k+1}(\perp)</script><p>（2）Least Fixed Point（数归法，证明最小）</p>
<p>假设我们有另一个不动点x，i.e., $x=f(x)$</p>
<p>由$\perp$的定义，我们有$\perp \sqsubseteq x$;</p>
<p>下面用数归法证明：</p>
<p>由于 $f$ 是单调的，因此</p>
<script type="math/tex; mode=display">
f(\perp) \sqsubseteq f(x)</script><p>对于$f^i(\perp)\sqsubseteq f^i(x)$，由于 $f$ 是单调的，因此有</p>
<script type="math/tex; mode=display">
f^{i+1}(\perp)\sqsubseteq f^{i+1}(x)</script><p>因此对于任意i，有</p>
<script type="math/tex; mode=display">
f^i(\perp)\sqsubseteq f^i(x)</script><p>又因为$x=f(x)$，所以存在一个i，有$f^i(\perp)\sqsubseteq f^i(x)=x$，因此有</p>
<script type="math/tex; mode=display">
f^{Fix} = f^k(\perp) \sqsubseteq x</script><p>因此$f^i(\perp)$ 是最小不动点。</p>
<h1 id="Relate-lterative-Algorithm-to-Fixed-Point-Theorem"><a href="#Relate-lterative-Algorithm-to-Fixed-Point-Theorem" class="headerlink" title="Relate lterative Algorithm to Fixed Point Theorem"></a>Relate lterative Algorithm to Fixed Point Theorem</h1><p>如何将迭代算法和不动点定理联系起来？</p>
<ol>
<li>程序中每一个状态为一个product lattice</li>
<li>Transfer function和join/meet fucntion可以视为F</li>
</ol>
<p><img src="/pl-静态程序分析课程笔记（数据流分析-理论基础）/image-20200812205336289.png" alt="image-20200812205336289"></p>
<p>下面只需要证明Transfer function和 join/meet function均为单调的即可</p>
<ol>
<li><p>Transfer function是单调的，因为通过之前分析，所有Gen/Kill的函数都是单调的；</p>
</li>
<li><p>Join/meet function是单调的，证明如下</p>
<p>要证Join/meet function，就是要证$\forall x, y, z \in L, x \sqsubseteq y \Rightarrow x\sqcup z \sqsubseteq y \sqcup z$</p>
<p>由 $\sqcup$ 定义可得，$y \sqsubseteq y \sqcup z$，</p>
<p>由于$\sqsubseteq$传递性，$x \sqsubseteq y$，因此$x \sqsubseteq y \sqcup z$，因此 $y \sqcup z$ 是 $x$ 的上界，</p>
<p>注意到 $y \sqcup z$ 也是 $z$ 的上界，而$x\sqcup z$ 是 $x$ 和 $z$ 的最小上界，</p>
<p>因此 $ x \sqsubseteq y \Rightarrow x\sqcup z \sqsubseteq y \sqcup z$</p>
</li>
</ol>
<p><strong>讨论算法复杂度</strong></p>
<p>定义格的高度即从top至bottom的最长路径长，</p>
<blockquote>
<p>The height of a lattice $h$ is the length of the longest path from Top to Bottom in the lattice.</p>
</blockquote>
<p>最坏情况即一次迭代，只变化一个单位高度，因此复杂度为$O(h \times k)$.</p>
<h1 id="May-Must-Analysis-A-Lattice-View"><a href="#May-Must-Analysis-A-Lattice-View" class="headerlink" title="May/Must Analysis, A Lattice View*"></a>May/Must Analysis, A Lattice View*</h1><p>任何分析初始状态都从unsafe至safe。</p>
<p>个人对safe和unsafe的理解：针对于分析结果而言，处理所有分析结果后，程序行为正常为safe，反之为unsafe，极端的safe是无用的（如安全扫描中的模式匹配）<br><img src="/pl-静态程序分析课程笔记（数据流分析-理论基础）/image-20200812214731510.png" alt="image-20200812214731510"></p>
<p>Must和May分析的示意图如上图所示，对于Must分析，每个代码块都是从 $\top$ 开始的，因为在程序一开始，算法认为所有的待分析对象都是“合格”的（例如存活表达式分析中，算法认为每个表达式都是成活的）——这是一个不安全的状态，经过不断迭代，算法逐渐下降到最大不动点，虽然已经过了truth点（漏报），但是这已经是最好情况了（越往下走越safe但是结果也没意义了），对这些结果做优化能确保程序不出错（safe）。</p>
<p>对于May分析，每个代码块从 $\perp$ 开始，即在一开始，算法认为所有分析对象都是不合格的（例如定义可达性分析中，算法认为每一条定义都没有新的定义）——这是May类型的不安全状态，经过不断迭代，算法逐渐上升到最小不动点，同样也过了truth（误报），这也是分析的最好情况，算法依旧停留在safe区域。</p>
<h1 id="Distributivity（分配性）-and-MOP"><a href="#Distributivity（分配性）-and-MOP" class="headerlink" title="Distributivity（分配性） and MOP"></a>Distributivity（分配性） and MOP</h1><h2 id="MOP（Meet-Over-All-Paths-Solution）"><a href="#MOP（Meet-Over-All-Paths-Solution）" class="headerlink" title="MOP（Meet-Over-All-Paths Solution）"></a>MOP（Meet-Over-All-Paths Solution）</h2><p>设 $s_x$ 为每一个statments，设 $F_p$ 是一个路径 $P$ 上的 transfer function，那么$MOP[S_i]=\sqcup/\sqcap_{\text{A path }P\text{ from Entry to }S_{i}} F_p(OUT[Entry])$.</p>
<p><img src="/pl-静态程序分析课程笔记（数据流分析-理论基础）/image-20200814215920162.png" alt="image-20200814215920162"></p>
<p>就是说，之前数据流分析的结果是<strong>流敏感</strong>的，而 MOP 的结果是路径敏感的，</p>
<p>例如下图所示的数据流，数据流分析的结果是 $\mathrm{IN}\left[\mathrm{s}_{4}\right]=f_{s_{3}}\left(f_{s_{1}}(\mathrm{OUT}[ entry ]) \sqcup f_{S_{2}}( OUT [ Entry ])\right)$，而MOP是 $ \mathrm{MOP}\left[\mathrm{s}_{4}\right]=f_{S_{3}}\left(f_{s_{1}}(\mathrm{OUT}[ entry ])\right) \sqcup f_{S_{3}}\left(f_{S_{2}}(\mathrm{OUT}[ Entry ])\right)$（注意$f_{s_3}$的位置）</p>
<p><img src="/pl-静态程序分析课程笔记（数据流分析-理论基础）/image-20200814220329588.png" alt="image-20200814220329588" style="zoom:50%;"></p>
<h2 id="Iterative-Algorithm-v-s-MOP"><a href="#Iterative-Algorithm-v-s-MOP" class="headerlink" title="Iterative Algorithm v.s. MOP"></a>Iterative Algorithm v.s. MOP</h2><p>MOP比Iterative分析更精确，也就是说路径敏感比敏感更精确，下面为证明（这里只需证明两条路径的情况，其它数归即可）：</p>
<p>由 $\sqcup$ 的定义得 $\mathrm{x} \sqsubseteq \mathrm{x} \sqcup \mathrm{y}$ 且 $\mathrm{y} \sqsubseteq \mathrm{x} \sqcup \mathrm{y}$；</p>
<p>因为 $F$ 是单调的，因此有 $F(x) \sqsubseteq F(x \sqcup y)$ 且 $F(y) \sqsubseteq F(x \sqcup y)$；</p>
<p>因此$F(x\sqcup y)$ 是 $F(x)$ 和 $F(y)$ 的上界；</p>
<p>又因为$F(x)\sqcup F(y)$是 $F(x)$ 和 $F(y)$ 的最小上界；</p>
<p>因此 $ F(x) \sqcup F(y) \sqsubseteq F(x\sqcup y)$，即$MOP \sqsubseteq Ours$。</p>
<p>然而，当F是distributive（F满足分配率）时，Interative和MOP一样准确。</p>
<p>BitVector或是Gen/Kill问题（set union/intersection for join/meet）都是满足分配率的</p>
<h1 id="Constant-Propagation"><a href="#Constant-Propagation" class="headerlink" title="Constant Propagation"></a>Constant Propagation</h1><blockquote>
<p>Given a variable $x$ at program point p, determine whether $x$ is guaranteed to hold a constant value at $p$</p>
</blockquote>
<p>对于在程序点 $p$ 的一个变量 $x$，判断 $x$ 是否为在 $p$ 点为一个常量</p>
<p>分析结果：对于每一个CFG节点，对应一个 $(x,v)$ 集合，$x$ 是变量，$v$ 是 $x$ 的值</p>
<h2 id="Lattice"><a href="#Lattice" class="headerlink" title="Lattice"></a>Lattice</h2><p>Domain： UNDEF → {…, -2, -1, 0, 1, 2, …} → NAC ，→ 表示 $\sqsubseteq$ 关系</p>
<p>Meet Operator $\sqcap$：</p>
<ul>
<li>$\mathrm{NAC} \sqcap v= \mathrm{NAC}$</li>
<li>$\mathrm{UNDEF} \sqcap v= v$</li>
<li>$c \sqcap v= \mathrm{NAC}$ （c 为一常量）</li>
<li>$c \sqcap c= c$</li>
<li>$c_1 \sqcap c_2 = \mathrm{NAC}$</li>
</ul>
<h2 id="Transfer-Function"><a href="#Transfer-Function" class="headerlink" title="Transfer Function"></a>Transfer Function</h2><p>讨论transfer function，对于一个赋值语句 <code>s: x= ...</code> 来说，定义其 F 为</p>
<script type="math/tex; mode=display">F: \mathrm{OUT}[s]=gen \cup(\mathrm{IN}[s]-\{(x, \_)\})</script><ul>
<li><code>s: x=c;</code>  $gen=\{(x,c)\}$</li>
<li><code>s: x=y;</code> $gen=\{(x, val(y))\}$</li>
<li><code>s: x=y op z;</code> $gen=\{(x, f(x,z))\}$ </li>
</ul>
<p>而 $f(x,z)$ 有三种情况：</p>
<script type="math/tex; mode=display">
f(y,z)=\left\{
\begin{array}{ll} val(y) \text { op } val(z) & \text {// if val(y) and val(z) are constants } \\ 
\text { NAC } & \text {//if val(y) or val(z) is NAC } \\
\text { UNDEF } & \text {// otherwise } \\
\end{array}\right.</script><h2 id="function不满足分配性"><a href="#function不满足分配性" class="headerlink" title="function不满足分配性"></a>function不满足分配性</h2><p>如下图所示，$F(X\sqcap Y)$ 中C的值为<strong>NAC</strong>，而$F(X) \sqcap F(Y)$中 C 的值为<strong>10</strong>，因此F不满足分配性。</p>
<p><img src="/pl-静态程序分析课程笔记（数据流分析-理论基础）/image-20200815173321586.png" alt="image-20200815173321586"></p>
<h1 id="Worklist-Algorithm"><a href="#Worklist-Algorithm" class="headerlink" title="Worklist Algorithm"></a>Worklist Algorithm</h1><p>Iterative Algorithm的优化，Iterative 存在冗余的计算，而Worklist只计算有变化的node：</p>
<figure class="highlight python"><table><tr><td class="gutter"><pre><span class="line">1</span><br><span class="line">2</span><br><span class="line">3</span><br><span class="line">4</span><br><span class="line">5</span><br><span class="line">6</span><br><span class="line">7</span><br><span class="line">8</span><br><span class="line">9</span><br><span class="line">10</span><br><span class="line">11</span><br></pre></td><td class="code"><pre><span class="line">OUT[entry] =∅;</span><br><span class="line"><span class="keyword">for</span>(each basic block B\entry) </span><br><span class="line">	OUT[B] =∅;</span><br><span class="line">    Worklist←all basic blocks</span><br><span class="line">	<span class="keyword">while</span> (Worklist <span class="keyword">is</span> notempty) </span><br><span class="line">    	Pick a basic block B <span class="keyword">from</span> Worklist</span><br><span class="line">		old_OUT= OUT[B]</span><br><span class="line">        IN[B] =⊔OUT[P]; <span class="comment"># join/meet P为B的前置代码块</span></span><br><span class="line">        OUT[B] = genB U (IN[B] - killB); <span class="comment"># transfer function </span></span><br><span class="line">        <span class="keyword">if</span>(old_OUT≠OUT[B])</span><br><span class="line">        	Add all successors of B to Worklis</span><br></pre></td></tr></table></figure>
<h1 id="分析特性"><a href="#分析特性" class="headerlink" title="分析特性"></a>分析特性</h1><ul>
<li>流敏感：程序语句随意调换位置，分析结果不变为流非敏感，否则为流敏感；</li>
<li>路径敏感：考虑程序中路径的可行性；</li>
<li></li>
</ul>
<h1 id="总结"><a href="#总结" class="headerlink" title="总结"></a>总结</h1><p>本节课主要介绍格，接着用格抽象描述数据流分析，解释为什么迭代算法能够到达最大/最小不动点，接着比较了流敏感和路径敏感的准确性，最后介绍worklist算法，以提升迭代算法的效率。</p>

    </div>

    
    
    
        
      
        

<div>
<ul class="post-copyright">
  <li class="post-copyright-author">
    <strong>本文作者： </strong>Anemone</li>
  <li class="post-copyright-link">
    <strong>本文链接：</strong>
    <a href="http://anemone.top/pl-静态程序分析课程笔记（数据流分析-理论基础）/" title="静态程序分析课程笔记（数据流分析-理论基础）">http://anemone.top/pl-静态程序分析课程笔记（数据流分析-理论基础）/</a>
  </li>
  <li class="post-copyright-license">
    <strong>版权声明： </strong>本博客所有文章除特别声明外，均采用 <a href="https://creativecommons.org/licenses/by-nc-sa/4.0/deed.zh" rel="noopener" target="_blank"><i class="fa fa-fw fa-creative-commons"></i>BY-NC-SA</a> 许可协议。转载请注明出处！</li>
</ul>
</div>

      

      <footer class="post-footer">
          
            
          
          <div class="post-tags">
            
              <a href="/tags/白盒扫描/" rel="tag"># 白盒扫描</a>
            
              <a href="/tags/静态程序分析/" rel="tag"># 静态程序分析</a>
            
              <a href="/tags/数据流分析/" rel="tag"># 数据流分析</a>
            
              <a href="/tags/PL/" rel="tag"># PL</a>
            
          </div>
        

        

          <div class="post-nav">
            <div class="post-nav-next post-nav-item">
              
                <a href="/pl-静态程序分析课程笔记（数据流分析-应用）/" rel="next" title="静态程序分析课程笔记（数据流分析-应用）">
                  <i class="fa fa-chevron-left"></i> 静态程序分析课程笔记（数据流分析-应用）
                </a>
              
            </div>

            <span class="post-nav-divider"></span>

            <div class="post-nav-prev post-nav-item">
              
                <a href="/pl-静态程序分析课程笔记（过程间分析）/" rel="prev" title="静态程序分析课程笔记（过程间分析）">
                  静态程序分析课程笔记（过程间分析） <i class="fa fa-chevron-right"></i>
                </a>
              
            </div>
          </div>
        
      </footer>
    
  </div>
  
  
  
  </article>

  </div>


          </div>
          
    
    <div class="comments" id="gitalk-container"></div>
  

        </div>
          
  
  <div class="sidebar-toggle">
    <div class="sidebar-toggle-line-wrap">
      <span class="sidebar-toggle-line sidebar-toggle-line-first"></span>
      <span class="sidebar-toggle-line sidebar-toggle-line-middle"></span>
      <span class="sidebar-toggle-line sidebar-toggle-line-last"></span>
    </div>
  </div>

  <aside class="sidebar">
    <div class="sidebar-inner">
        
        
        
        
      

      <ul class="sidebar-nav motion-element">
        <li class="sidebar-nav-toc">
          文章目录
        </li>
        <li class="sidebar-nav-overview">
          站点概览
        </li>
      </ul>

      <!--noindex-->
      <div class="post-toc-wrap sidebar-panel">
          <div class="post-toc motion-element"><ol class="nav"><li class="nav-item nav-level-1"><a class="nav-link" href="#Iterative-Algorithm"><span class="nav-number">1.</span> <span class="nav-text">Iterative Algorithm</span></a></li><li class="nav-item nav-level-1"><a class="nav-link" href="#Poset-amp-partial-order（偏序集和偏序）"><span class="nav-number">2.</span> <span class="nav-text">Poset &amp; partial order（偏序集和偏序）</span></a></li><li class="nav-item nav-level-1"><a class="nav-link" href="#Uppper-and-Lower-Bounds（上界和下界）"><span class="nav-number">3.</span> <span class="nav-text">Uppper and Lower Bounds（上界和下界）</span></a><ol class="nav-child"><li class="nav-item nav-level-2"><a class="nav-link" href="#最小上界、最大下界"><span class="nav-number">3.1.</span> <span class="nav-text">最小上界、最大下界</span></a></li></ol></li><li class="nav-item nav-level-1"><a class="nav-link" href="#Lattice-Semilattice-Complete-and-Product-Lattice"><span class="nav-number">4.</span> <span class="nav-text">Lattice, Semilattice, Complete and Product Lattice</span></a><ol class="nav-child"><li class="nav-item nav-level-2"><a class="nav-link" href="#Lattice（格）"><span class="nav-number">4.1.</span> <span class="nav-text">Lattice（格）</span></a></li><li class="nav-item nav-level-2"><a class="nav-link" href="#Semilattice"><span class="nav-number">4.2.</span> <span class="nav-text">Semilattice</span></a></li><li class="nav-item nav-level-2"><a class="nav-link" href="#Complete-Lattice，top-amp-bottom（全格，-top-和-perp-）"><span class="nav-number">4.3.</span> <span class="nav-text">Complete Lattice，top &amp; bottom（全格，$\top$ 和 $\perp$）*</span></a></li><li class="nav-item nav-level-2"><a class="nav-link" href="#Product-Lattice"><span class="nav-number">4.4.</span> <span class="nav-text">Product Lattice</span></a></li></ol></li><li class="nav-item nav-level-1"><a class="nav-link" href="#Data-Flow-Analysis-Framework-via-Lattice"><span class="nav-number">5.</span> <span class="nav-text">Data Flow Analysis Framework via Lattice</span></a></li><li class="nav-item nav-level-1"><a class="nav-link" href="#Monotonicity-and-Fixed-Point-Theorem"><span class="nav-number">6.</span> <span class="nav-text">Monotonicity and Fixed Point Theorem</span></a><ol class="nav-child"><li class="nav-item nav-level-2"><a class="nav-link" href="#Monotonicity（单调性）"><span class="nav-number">6.1.</span> <span class="nav-text">Monotonicity（单调性）</span></a></li><li class="nav-item nav-level-2"><a class="nav-link" href="#Fixed-Point-Theorem"><span class="nav-number">6.2.</span> <span class="nav-text">Fixed-Point Theorem</span></a></li></ol></li><li class="nav-item nav-level-1"><a class="nav-link" href="#Relate-lterative-Algorithm-to-Fixed-Point-Theorem"><span class="nav-number">7.</span> <span class="nav-text">Relate lterative Algorithm to Fixed Point Theorem</span></a></li><li class="nav-item nav-level-1"><a class="nav-link" href="#May-Must-Analysis-A-Lattice-View"><span class="nav-number">8.</span> <span class="nav-text">May/Must Analysis, A Lattice View*</span></a></li><li class="nav-item nav-level-1"><a class="nav-link" href="#Distributivity（分配性）-and-MOP"><span class="nav-number">9.</span> <span class="nav-text">Distributivity（分配性） and MOP</span></a><ol class="nav-child"><li class="nav-item nav-level-2"><a class="nav-link" href="#MOP（Meet-Over-All-Paths-Solution）"><span class="nav-number">9.1.</span> <span class="nav-text">MOP（Meet-Over-All-Paths Solution）</span></a></li><li class="nav-item nav-level-2"><a class="nav-link" href="#Iterative-Algorithm-v-s-MOP"><span class="nav-number">9.2.</span> <span class="nav-text">Iterative Algorithm v.s. MOP</span></a></li></ol></li><li class="nav-item nav-level-1"><a class="nav-link" href="#Constant-Propagation"><span class="nav-number">10.</span> <span class="nav-text">Constant Propagation</span></a><ol class="nav-child"><li class="nav-item nav-level-2"><a class="nav-link" href="#Lattice"><span class="nav-number">10.1.</span> <span class="nav-text">Lattice</span></a></li><li class="nav-item nav-level-2"><a class="nav-link" href="#Transfer-Function"><span class="nav-number">10.2.</span> <span class="nav-text">Transfer Function</span></a></li><li class="nav-item nav-level-2"><a class="nav-link" href="#function不满足分配性"><span class="nav-number">10.3.</span> <span class="nav-text">function不满足分配性</span></a></li></ol></li><li class="nav-item nav-level-1"><a class="nav-link" href="#Worklist-Algorithm"><span class="nav-number">11.</span> <span class="nav-text">Worklist Algorithm</span></a></li><li class="nav-item nav-level-1"><a class="nav-link" href="#分析特性"><span class="nav-number">12.</span> <span class="nav-text">分析特性</span></a></li><li class="nav-item nav-level-1"><a class="nav-link" href="#总结"><span class="nav-number">13.</span> <span class="nav-text">总结</span></a></li></ol></div>
        
      </div>
      <!--/noindex-->

      <div class="site-overview-wrap sidebar-panel">
        <div class="site-author motion-element" itemprop="author" itemscope itemtype="http://schema.org/Person">
    <img class="site-author-image" itemprop="image"
      src="/images/avatar.jpg"
      alt="Anemone">
  <p class="site-author-name" itemprop="name">Anemone</p>
  <div class="site-description" itemprop="description">关注Web安全、移动安全、Fuzz测试和机器学习</div>
</div>
<div class="site-state-wrap motion-element">
  <nav class="site-state">
      <div class="site-state-item site-state-posts">
        
          <a href="/archives/">
        
          <span class="site-state-item-count">70</span>
          <span class="site-state-item-name">日志</span>
        </a>
      </div>
    
      
      
      <div class="site-state-item site-state-categories">
        
          
            <a href="/categories/">
          
        
        <span class="site-state-item-count">31</span>
        <span class="site-state-item-name">分类</span>
        </a>
      </div>
    
      
      
      <div class="site-state-item site-state-tags">
        
          
            <a href="/tags/">
          
        
        <span class="site-state-item-count">86</span>
        <span class="site-state-item-name">标签</span>
        </a>
      </div>
    
  </nav>
</div>
  <div class="feed-link motion-element">
    <a href="/atom.xml" rel="alternate">
      <i class="fa fa-rss"></i>RSS
    </a>
  </div>
  <div class="links-of-author motion-element">
      <span class="links-of-author-item">
      
      
        
      
      
        
      
        <a href="https://github.com/anemone95" title="GitHub &rarr; https://github.com/anemone95" rel="noopener" target="_blank"><i class="fa fa-fw fa-github"></i>GitHub</a>
      </span>
    
      <span class="links-of-author-item">
      
      
        
      
      
        
      
        <a href="mailto:anemone95@qq.com" title="E-Mail &rarr; mailto:anemone95@qq.com" rel="noopener" target="_blank"><i class="fa fa-fw fa-envelope"></i>E-Mail</a>
      </span>
    
  </div>
  <div class="cc-license motion-element" itemprop="license">
    
  
    <a href="https://creativecommons.org/licenses/by-nc-sa/4.0/deed.zh" class="cc-opacity" rel="noopener" target="_blank"><img src="/images/cc-by-nc-sa.svg" alt="Creative Commons"></a>
  </div>



      </div>

    </div>
  </aside>
  <div id="sidebar-dimmer"></div>


      </div>
    </main>

    <footer id="footer" class="footer">
      <div class="footer-inner">
        <div class="copyright">&copy; 2018 – <span itemprop="copyrightYear">2020</span>
  <span class="with-love" id="animate">
    <i class="fa fa-user"></i>
  </span>
  <span class="author" itemprop="copyrightHolder">anemone</span>
</div>
  <div class="powered-by">由 <a href="https://hexo.io" class="theme-link" rel="noopener" target="_blank">Hexo</a> 强力驱动 v3.9.0</div>
  <span class="post-meta-divider">|</span>
  <div class="theme-info">主题 – <a href="https://theme-next.org" class="theme-link" rel="noopener" target="_blank">NexT.Pisces</a> v7.4.0</div>

        






  
  <script>
  function leancloudSelector(url) {
    return document.getElementById(url).querySelector('.leancloud-visitors-count');
  }
  if (CONFIG.page.isPost) {
    function addCount(Counter) {
      var visitors = document.querySelector('.leancloud_visitors');
      var url = visitors.getAttribute('id').trim();
      var title = visitors.getAttribute('data-flag-title').trim();

      Counter('get', `/classes/Counter?where=${JSON.stringify({ url })}`)
        .then(response => response.json())
        .then(({ results }) => {
          if (results.length > 0) {
            var counter = results[0];
            Counter('put', '/classes/Counter/' + counter.objectId, { time: { '__op': 'Increment', 'amount': 1 } })
              .then(response => response.json())
              .then(() => {
                leancloudSelector(url).innerText = counter.time + 1;
              })
            
              .catch(error => {
                console.log('Failed to save visitor count', error);
              })
          } else {
              Counter('post', '/classes/Counter', { title: title, url: url, time: 1 })
                .then(response => response.json())
                .then(() => {
                  leancloudSelector(url).innerText = 1;
                })
                .catch(error => {
                  console.log('Failed to create', error);
                });
            
          }
        })
        .catch(error => {
          console.log('LeanCloud Counter Error', error);
        });
    }
  } else {
    function showTime(Counter) {
      var visitors = document.querySelectorAll('.leancloud_visitors');
      var entries = [...visitors].map(element => {
        return element.getAttribute('id').trim();
      });

      Counter('get', `/classes/Counter?where=${JSON.stringify({ url: { '$in': entries } })}`)
        .then(response => response.json())
        .then(({ results }) => {
          if (results.length === 0) {
            document.querySelectorAll('.leancloud_visitors .leancloud-visitors-count').forEach(element => {
              element.innerText = 0;
            });
            return;
          }
          for (var i = 0; i < results.length; i++) {
            var item = results[i];
            var url = item.url;
            var time = item.time;
            leancloudSelector(url).innerText = time;
          }
          for (var i = 0; i < entries.length; i++) {
            var url = entries[i];
            var element = leancloudSelector(url);
            if (element.innerText == '') {
              element.innerText = 0;
            }
          }
        })
        .catch(error => {
          console.log('LeanCloud Counter Error', error);
        });
    }
  }

  fetch('https://app-router.leancloud.cn/2/route?appId=o5UaCJdPfEG0g7MVxXSMagpT-gzGzoHsz')
    .then(response => response.json())
    .then(({ api_server }) => {
      var Counter = (method, url, data) => {
        return fetch(`https://${api_server}/1.1${url}`, {
          method: method,
          headers: {
            'X-LC-Id': 'o5UaCJdPfEG0g7MVxXSMagpT-gzGzoHsz',
            'X-LC-Key': 'c6IN1PuMV3QPltJcrHfn74Gt',
            'Content-Type': 'application/json',
          },
          body: JSON.stringify(data)
        });
      };
      if (CONFIG.page.isPost) {
        const localhost = /http:\/\/(localhost|127.0.0.1|0.0.0.0)/;
        if (localhost.test(document.URL)) return;
        addCount(Counter);
      } else if (document.querySelectorAll('.post-title-link').length >= 1) {
        showTime(Counter);
      }
    });
  </script>






        
      </div>
    </footer>
  </div>

  
  <script src="//cdn.jsdelivr.net/npm/animejs@3.1.0/lib/anime.min.js"></script>
  <script src="https://cdn.bootcss.com/velocity/1.2.1/velocity.min.js"></script>
  <script src="https://cdn.bootcss.com/velocity/1.2.1/velocity.ui.js"></script>
<script src="/js/utils.js?v=7.4.0"></script><script src="/js/motion.js?v=7.4.0"></script>
<script src="/js/schemes/pisces.js?v=7.4.0"></script>
<script src="/js/next-boot.js?v=7.4.0"></script>



  
  <script>
    (function(){
      var bp = document.createElement('script');
      var curProtocol = window.location.protocol.split(':')[0];
      bp.src = (curProtocol === 'https') ? 'https://zz.bdstatic.com/linksubmit/push.js' : 'http://push.zhanzhang.baidu.com/push.js';
      var s = document.getElementsByTagName("script")[0];
      s.parentNode.insertBefore(bp, s);
    })();
  </script>








  
<link rel="stylesheet" href="//cdn.jsdelivr.net/npm/instantsearch.js@2.10.4/dist/instantsearch.min.css">
<script src="//cdn.jsdelivr.net/npm/instantsearch.js@2.10.4/dist/instantsearch.min.js"></script><script src="/js/algolia-search.js?v=7.4.0"></script>











<script>
if (document.querySelectorAll('pre.mermaid').length) {
  NexT.utils.getScript('//cdn.bootcss.com/mermaid/8.2.6/mermaid.min.js', () => {
    mermaid.initialize({
      theme: 'forest',
      logLevel: 3,
      flowchart: { curve: 'linear' },
      gantt: { axisFormat: '%m/%d/%Y' },
      sequence: { actorMargin: 50 }
    });
  }, window.mermaid);
}
</script>




  

  
    
      
<script type="text/x-mathjax-config">

  MathJax.Hub.Config({
    tex2jax: {
      inlineMath: [ ['$', '$'], ['\\(', '\\)'] ],
      processEscapes: true,
      skipTags: ['script', 'noscript', 'style', 'textarea', 'pre', 'code']
    },
    TeX: {
      equationNumbers: {
        autoNumber: 'AMS'
      }
    }
  });

  MathJax.Hub.Register.StartupHook('TeX Jax Ready', function() {
    MathJax.InputJax.TeX.prefilterHooks.Add(function(data) {
      if (data.display) {
        var next = data.script.nextSibling;
        while (next && next.nodeName.toLowerCase() === '#text') {
          next = next.nextSibling;
        }
        if (next && next.nodeName.toLowerCase() === 'br') {
          next.parentNode.removeChild(next);
        }
      }
    });
  });

  MathJax.Hub.Queue(function() {
    var all = MathJax.Hub.getAllJax(), i;
    for (i = 0; i < all.length; i += 1) {
      element = document.getElementById(all[i].inputID + '-Frame').parentNode;
      if (element.nodeName.toLowerCase() == 'li') {
        element = element.parentNode;
      }
      element.classList.add('has-jax');
    }
  });
</script>
<script>
  NexT.utils.getScript('//cdn.bootcss.com/mathjax/2.7.1/latest.js?config=TeX-AMS-MML_HTMLorMML', () => {
    MathJax.Hub.Typeset();
  }, window.MathJax);
</script>

    
  

  

  

<link rel="stylesheet" href="//cdn.jsdelivr.net/npm/gitalk@1/dist/gitalk.min.css">

<script>
  NexT.utils.getScript('//cdn.jsdelivr.net/npm/gitalk@1/dist/gitalk.min.js', () => {
    var gitalk = new Gitalk({
      clientID: 'f3075553d7b0225df6ca',
      clientSecret: '68362ba87c4cc8e13103afcf729f5bd8ea176a78',
      repo: 'anemone95.github.io',
      owner: 'Anemone95',
      admin: ['Anemone95'],
      id: '0aacf840e4adfcb1ce7d31dd6311031c',
        language: window.navigator.language || window.navigator.userLanguage,
      
      distractionFreeMode: 'true'
    });
    gitalk.render('gitalk-container');
  }, window.Gitalk);
</script>

</body>
</html>
